When designing integrated circuits including combinatorial and sequential gates and circuit elements, tools are used to check the integrity of the final design before proceeding to mass-production. The tools are computer programs which require as input a mathematical model of the integrated circuit design and a specification of desired design criteria. Thus, for example, a Flip-Flop circuit element may generate an acknowledge signal (ACK) responsive to a request signal (REQ) and the design specification may require that the REQ signal produces the ACK signal within three clock cycles.
From knowledge of the design specification and the mathematical model of the integrated circuit, the computer determines whether the model meets the specified design criteria. Such a program solves a state machine having a large number of variables dependent, of course, on the model complexity. Thus, the more gates and memory elements in the integrated circuit, the more complex is the model and the greater the number of variables in the state machine to be solved. In practice, the more complex the design the greater is the size of memory which the computer requires to solve the state machine; and the longer the calculation time. There exists, therefore, a need to reduce the model complexity without compromising on the integrity of the model checking.
Prior art techniques relate principally to manual and/or trivial reduction of the number of state variables by eliminating obviously redundant circuit elements. For example, FIG. 1 shows part of a logic circuit depicted generally as 10 comprising an AND-gate 11 whose output is fed to the REQ input of a Flip-Flop 12 having an ACK output 13 and a CLK input 14. A first input 15 of the AND-gate 11 is driven by the output of a sub-circuit designated 16 which may itself include a large number of logic elements. A second input 17 of the AND-gate 11 is tied to logic "0".
In such an arrangement, the output of the AND-gate 11 will always be logic "0" regardless of any changes that occur in the logic state of the first input 15 of the AND-gate 11 consequent to operation of the sub-circuit 16. In this trivial example, the AND-gate 11 as well as the Flip-Flop 12 may be replaced by a line of constant logic level "0" thereby reducing the number of state space variables in the mathematical model representative of the logic circuit 10.
Another example of useful reduction is the elimination of signals that are not in the so-called "cone of influence" of the circuit being verified. Thus, if only part of the circuit is being verified, then any other parts whose behavior does not alter the part under verification can be eliminated. Thus, in the example shown in FIG. 1, suppose that only that part of the logic circuit 10 which is connected to the ACK output 13 of the Flip-Flop 12 is being verified. In such case, not only can the AND-gate 11 and the Flip-Flop 12 be replaced by a line of constant logic level "0", but the sub-circuit 16 can be eliminated altogether. This follows since the sub-circuit 16 is not in the cone of logic being verified. This, of course, significantly reduces the complexity of the model being tested resulting in faster processing time and lower memory requirements.
However, it is not always convenient or possible to reduce the number of space state variables in such manner and even when manual reduction is feasible, it is only amenable to obvious or trivial reductions. Non-obvious reductions may still be possible and in this case conventional manual techniques do not succeed in optimal reduction. It would thus be desirable to offer a systematic approach to model reduction suitable for computer-implementation allowing non-obvious reductions to be achieved and thus achieving optimal reduction and maximum saving of computer resources.